1. Field of the Invention
The present invention relates to programming languages for computer systems. More specifically, the present invention relates to a method and an apparatus that facilitate expressing type relationships and using the expressed type relationships to check the type soundness of a program.
2. Related Art
As computer programs grow increasingly more complicated, it is becoming progressively harder to ensure that such programs operate reliably. Software developers typically rely on type-checking mechanisms within compilers or interpreters to reduce the number of runtime errors that occur when a computer program executes. These type-checking mechanisms are typically supported by corresponding type-related programming language features, which allow type relationships to be expressed for various data items and functions within a program.
Some programming languages support “parametric types,” which can be expressed using type parameters. Parametric types enable greater precision of type checking and can also reduce code duplication. However, many formulations of parametric types require significant verbosity and place severe limits on expressible type relationships. For example, in programming languages with nominal subtyping, including Eiffel, C#, and the Java™ Programming Language, it is often required to explicitly instantiate more type parameters than is necessary to infer a full type instantiation. It is also difficult to express useful type relationships among instantiations, relationships such as covariance and contravariance, without additional language primitives. Conventional type-inference techniques provide only a partial solution to the former problem, and offer no help with the latter.
Hence, what is needed is a method and an apparatus for expressing and checking type relationships without the above-described problems.